\begin{tabbing}
$\forall$${\it es}$:ES, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $T$:Type, $i$:Id, $f$:(State(${\it ds}$)$\rightarrow$$T$).
\\[0ex]($\forall$$x$, $y$:$T$. Dec($x$ $=$ $y$))
\\[0ex]$\Rightarrow$ ($\forall$$x$:Id. vartype($i$;$x$) $\subseteq\rho$ ${\it ds}$($x$)?Top)
\\[0ex]$\Rightarrow$ \=$\forall$${\it e'}$@$i$.\+
\\[0ex]($\forall$$e$:E. $e$ $\leq$ ${\it e'}$  $\Rightarrow$ $f$((state when $e$)) $=$ $f$(state after ${\it e'}$) $\in$ $T$)
\\[0ex]$\vee$ (\=$\exists$$e$:E.\+
\\[0ex]$e$ $\leq$ ${\it e'}$ 
\\[0ex]\& \=$\neg$$f$((state when $e$)) $=$ $f$(state after ${\it e'}$)\+
\\[0ex]\& (\=$\forall$${\it e''}$:E.\+
\\[0ex]($e$ $<$loc ${\it e''}$) $\Rightarrow$ ${\it e''}$ $\leq$ ${\it e'}$  $\Rightarrow$ $f$((state when ${\it e''}$)) $=$ $f$(state after ${\it e'}$) $\in$ $T$))
\-\-\-\-
\end{tabbing}